MAYBE
* Step 1: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          compare_list#2(Cons(x4,x2),Nil()) -> False()
          compare_list#2(Cons(x8,x6),Cons(x4,x2)) -> ite2#3(eqNat#2(x8,x4),compare_list#2(x6,x2),leqNat#2(x8,x4))
          compare_list#2(Nil(),x2) -> True()
          cond_mergesort_compare_log_l_l_2(Pair(Cons(x4,x5),Cons(x2,x3)),x1) -> merge#3(mergesort#3(x1,Cons(x4,x5))
                                                                                       ,mergesort#3(x1,Cons(x2,x3)))
          cond_split_l_2(Pair(x11,x12),x7,x9) -> Pair(Cons(x7,x11),Cons(x9,x12))
          eqNat#2(0(),0()) -> True()
          eqNat#2(0(),S(x16)) -> False()
          eqNat#2(S(x16),0()) -> False()
          eqNat#2(S(x4),S(x2)) -> eqNat#2(x4,x2)
          ite2#3(False(),x48,x56) -> x56
          ite2#3(True(),x48,x56) -> x48
          ite_b#2(False(),Cons(x6,x8),Cons(x2,x4)) -> Cons(x2,x4)
          ite_b#2(True(),Cons(x6,x8),Cons(x2,x4)) -> Cons(x6,x8)
          leqNat#2(x4,0()) -> True()
          leqNat#2(0(),S(x12)) -> False()
          leqNat#2(S(x4),S(x2)) -> leqNat#2(x4,x2)
          main(x1) -> mergesort#3(S(S(S(S(S(S(0())))))),x1)
          merge#3(Cons(x18,x14),Cons(x10,x6)) -> ite_b#2(compare_list#2(x18,x10)
                                                        ,Cons(x18,merge#3(x14,Cons(x10,x6)))
                                                        ,Cons(x10,merge#3(Cons(x18,x14),x6)))
          merge#3(Cons(x4,x2),Nil()) -> Cons(x4,x2)
          merge#3(Nil(),x2) -> x2
          mergesort#3(0(),Cons(x1,x2)) -> Nil()
          mergesort#3(S(x12),Cons(x112,Cons(x144,x160))) ->
            cond_mergesort_compare_log_l_l_2(cond_split_l_2(split#1(x160),x112,x144),x12)
          mergesort#3(S(x4),Cons(x8,Nil())) -> Cons(x8,Nil())
          mergesort#3(S(S(S(S(S(S(0())))))),Nil()) -> bot[0]()
          split#1(Cons(x14,Cons(x18,x20))) -> cond_split_l_2(split#1(x20),x14,x18)
          split#1(Cons(x14,Nil())) -> Pair(Cons(x14,Nil()),Nil())
          split#1(Nil()) -> Pair(Nil(),Nil())
      - Signature:
          {compare_list#2/2,cond_mergesort_compare_log_l_l_2/2,cond_split_l_2/3,eqNat#2/2,ite2#3/3,ite_b#2/3
          ,leqNat#2/2,main/1,merge#3/2,mergesort#3/2,split#1/1} / {0/0,Cons/2,False/0,Nil/0,Pair/2,S/1,True/0
          ,bot[0]/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {compare_list#2,cond_mergesort_compare_log_l_l_2
          ,cond_split_l_2,eqNat#2,ite2#3,ite_b#2,leqNat#2,main,merge#3,mergesort#3,split#1} and constructors {0,Cons
          ,False,Nil,Pair,S,True,bot[0]}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE